Lógica proposicional

El módulo sympy permite hacer algunos cálculos en lógica proposicional



In [1]:

    
from sympy import *

Vamos a decirle a sympy que renderice las salidas en LaTeX con mathjax



In [2]:

    
init_printing()

Satisfacibilidad

Ejemplo Si es cierto $a\to b$, ¿podemos inferir algo sobre $a\vee c\to b\vee c$? ¿Y sobre $a\wedge c\to b\wedge c$?



In [3]:

    
a,b,c = symbols("a,b,c")

Vamos a usar que $\Gamma \models \alpha$ equivale a que $\Gamma\cup\{\neg \alpha\}$ es insatisfacible



In [4]:

    
p = a >> b
q = (a|c)>>(b|c)



In [5]:

    
p&~q









    Out[5]:





$$\left(a \Rightarrow b\right) \wedge \left(a \vee c\right) \not\Rightarrow \left(b \vee c\right)$$



In [6]:

    
satisfiable(p&~q)









    Out[6]:





False

También podíamos ver si $p\to q$ es una tautología por el teorema de la deducción, o lo que es lo mismo, mostrar que siempre es verdadera



In [7]:

    
simplify(p>>q)









    Out[7]:





$$\mathrm{True}$$

Lo mismo con $a\wedge c\to b\wedge c$



In [8]:

    
simplify(p>>((a&c)>>(b&c)))









    Out[8]:





$$\mathrm{True}$$

Ejemplo Estudia si el conjunto $\{c\to (a\vee c), b\to(c\to a), d\wedge \neg (c\to a)\}$ es satisfacible



In [9]:

    
a,b,c,d = symbols("a,b,c,d")



In [10]:

    
satisfiable((c>>(a|b))&(b>>(c>>a))&d&~(c>>a))









    Out[10]:





False

De ser satisfacible, nos daría un mundo donde lo es



In [11]:

    
satisfiable(a|b)









    Out[11]:





{b: True, a: True}

O bien todos los mundos donde lo es, si así se lo pedimos



In [12]:

    
list(satisfiable(a|b, all_models=True))









    Out[12]:





[{b: True, a: True}, {b: False, a: True}, {b: True, a: False}]

Implicación semántica

Podemos detectar si $\Gamma\models a$ con la siguiente función



In [13]:

    
def implica(gamma,a):
    """ Determina si Gamma implica semanticamente a"""
    p = True
    for x in gamma:
        p = p & x
    p=p&(~a)
    return not(satisfiable(p))



In [14]:

    
implica([a,a>>b],b)









    Out[14]:





True



In [15]:

    
implica([a>>b,b>>c],a>>c)









    Out[15]:





True

Volvamos al primer ejemplo



In [16]:

    
implica([a>>b], (a|c)>>(b|c))









    Out[16]:





True

Otro ejemplo



In [17]:

    
implica([a>>b],a)









    Out[17]:





False

Tautologías

Una proposición $a$ es tautología si $\models a$



In [18]:

    
implica([], a>>(b>>a))









    Out[18]:





True



In [19]:

    
implica([],~a>>(a>>b))









    Out[19]:





True



In [20]:

    
def tautologia(a):
    return not(satisfiable(~a))



In [21]:

    
tautologia(~a>>(a>>b))









    Out[21]:





True



In [22]:

    
tautologia(a>>b)









    Out[22]:





False



In [23]:

    
(a>>b).args









    Out[23]:





$$\left ( a, \quad b\right )$$



In [24]:

    
to_cnf(a>>(b&c))









    Out[24]:





$$\left(b \vee \neg a\right) \wedge \left(c \vee \neg a\right)$$



In [25]:

    
type(_)









    Out[25]:





And



In [26]:

    
to_cnf(a>>b)









    Out[26]:





$$b \vee \neg a$$



In [27]:

    
type(_)









    Out[27]:





Or

Davis-Putnam

Forma clausular y operaciones con literales

Vamos a definir la forma clausular de un conjunto de proposiciones



In [28]:

    
G= {c>>(a|b), b>>(c>>a), d&~(c>>a)}



In [29]:

    
def forma_clausular(G):
    fc = set([])
    for g in G:
        q = to_cnf(g)
        if isinstance(q,And):
            fc.update(q.args)
        else:
            fc.add(q)
    return fc



In [30]:

    
forma_clausular(G)









    Out[30]:





$$\left\{c, d, \neg a, a \vee b \vee \neg c, a \vee \neg b \vee \neg c\right\}$$



In [31]:

    
def es_literal(p):
    if isinstance(p,Symbol):
        return True
    if isinstance(p,Not):
        ar = p.args
        if len(ar)==1 and isinstance(ar[0],Symbol):
            return True
    return False



In [32]:

    
es_literal(a)









    Out[32]:





True



In [33]:

    
es_literal(~a)









    Out[33]:





True



In [34]:

    
es_literal(a&b)









    Out[34]:





False



In [35]:

    
v=Or(*[])



In [36]:

    
type(v)









    Out[36]:





sympy.logic.boolalg.BooleanFalse



In [37]:

    
v==False









    Out[37]:





True



In [38]:

    
def es_clausula(p):
    if p==False:
        return True
    if es_literal(p):
        return True
    if isinstance(p,Or):
        ar = p.args
        return all(es_literal(a) for a in ar)
    return False



In [39]:

    
es_clausula(a&b)









    Out[39]:





False



In [40]:

    
es_clausula(a|~b)









    Out[40]:





True



In [41]:

    
def complemento(p):
    if isinstance(p,Symbol):
        return ~p
    if isinstance(p,Not):
        return p.args[0]
    return None



In [42]:

    
complemento(a)









    Out[42]:





$$\neg a$$



In [43]:

    
complemento(~a)









    Out[43]:





$$a$$



In [44]:

    
l=[1,2,3]
l.remove(3)
2 in l









    Out[44]:





True



In [45]:

    
def quita(c,l):
    if c==False:
        return False
    if es_literal(c):
        if c==l:
            return False
        return c
    ar = list(c.args)
    if l in ar:
        ar.remove(l)
        return Or(*ar)
    return c



In [46]:

    
quita(a|b,b)









    Out[46]:





$$a$$



In [47]:

    
quita(a|b,~b)









    Out[47]:





$$a \vee b$$



In [48]:

    
def primero(xs,cond):
    for x in xs:
        if cond(x):
            return x
    return None



In [49]:

    
primero([1,2,3],lambda x:(x%2)==0)









    Out[49]:





$$2$$



In [50]:

    
def clausula_a_lista(c):
    if c==False:
        return []
    if es_literal(c):
        return [c]
    return list(c.args)



In [51]:

    
clausula_a_lista(a|b|~c)









    Out[51]:





$$\left [ a, \quad b, \quad \neg c\right ]$$

Detectando una clausula unit



In [52]:

    
def clausula_unit(cs):
    l = primero(cs,es_literal)
    if l!=None:
        print("Hemos encontrado una clausula unit ", l)
        csp = [c for c in cs if not(l in clausula_a_lista(c))]
        cspq = [quita(c,complemento(l)) for c in csp]
        pprint(cspq)
        return cspq
    return cs



In [53]:

    
clausula_unit([a,a|b, ~a|c, c|b])









    



Hemos encontrado una clausula unit  a
[c, b ∨ c]






    Out[53]:





$$\left [ c, \quad b \vee c\right ]$$



In [54]:

    
Or(a,~a,b)









    Out[54]:





$$a \vee b \vee \neg a$$



In [55]:

    
simplify(_)









    Out[55]:





$$\mathrm{True}$$

Quitando tautologías y cláusulas redundantes



In [56]:

    
def quita_tautologias(cs):
    return [c for c in cs if simplify(c)!=True]



In [57]:

    
quita_tautologias([a|b|~a,a|c])









    Out[57]:





$$\left [ a \vee c\right ]$$



In [58]:

    
l=[1,2]

La siguiente función determina si todos los literales de una cláusula están contenidos en otra cláusula



In [59]:

    
def contenido(c1,c2):
    return all((l in clausula_a_lista(c2)) for l in clausula_a_lista(c1))



In [60]:

    
contenido(a|b,a|b|c)









    Out[60]:





True



In [61]:

    
contenido(a|b,a|c)









    Out[61]:





False



In [62]:

    
def quita_redundantes(cs):
    return [c for c in cs if not(any(contenido(d,c) and d!=c for d in cs))]



In [63]:

    
quita_redundantes([a|b,a|b|c])









    Out[63]:





$$\left [ a \vee b\right ]$$

Encontrando litereales puros



In [66]:

    
def literal_puro(cs):
    literales = set([])
    for c in cs:
        literales.update(clausula_a_lista(c))
    l = primero(literales, lambda x:not(complemento(x) in literales))
    if l==None:
        return cs
    print("Hemos encontrado un literal puro", l)
    csp = [c for c in cs if not(l in clausula_a_lista(c))]
    print(csp)
    return csp



In [67]:

    
literal_puro([a|b,~a])









    



Hemos encontrado un literal puro b
[Not(a)]






    Out[67]:





$$\left [ \neg a\right ]$$

Dividiendo cuando no hay literales puros ni cláuslas unit



In [68]:

    
def divide(cs):
    literales = set([])
    for c in cs:
        literales.update(clausula_a_lista(c))
    l = primero(literales, lambda x:(complemento(x) in literales))
    cl = complemento(l)
    csl = set([quita(c,l) for c in cs if l in clausula_a_lista(c)])
    csnl= set([quita(c,cl) for c in cs if cl in clausula_a_lista(c)])
    csc = set([c for c in cs if not(l in clausula_a_lista(c)) and not(cl in clausula_a_lista(c))])
    parte1=csl.union(csc)
    parte2=csnl.union(csc)
    print("Dividimos usando ",l)
    pprint(parte1)
    pprint(parte2)
    return [csl.union(csc),csnl.union(csc)]



In [69]:

    
divide([a|b,~a|b,a|c, b|c])









    



Dividimos usando  Not(a)
set([b, b ∨ c])
set([b, c, b ∨ c])






    Out[69]:





$$\left [ \left\{b, b \vee c\right\}, \quad \left\{b, c, b \vee c\right\}\right ]$$

Algoritmo de Davis-Putnam



In [70]:

    
def inconsistente(cs):
    """Detecta si cs es satisfacible usando Davis-Putnam"""
    css = quita_tautologias(quita_redundantes(cs))
    unitpuro=True
    while unitpuro:
        cssn = clausula_unit(css)
        if cssn== css:
            cssn = literal_puro(css)
            if cssn==css:
                unitpuro=False
        if len(cssn)==0:
            print("Hemos llegado al conjunto vacío")
            return False
        if False in cssn:
            print("Hemos encontrado la cláusula vacía")
            return True
        css=cssn

    d = divide(css)
    return inconsistente(d[0]) and inconsistente(d[1])



In [71]:

    
inconsistente([~a,a])









    



Hemos encontrado una clausula unit  Not(a)
[False]
Hemos encontrado la cláusula vacía






    Out[71]:





True



In [72]:

    
clausula_unit([a,b])









    



Hemos encontrado una clausula unit  a
[b]






    Out[72]:





$$\left [ b\right ]$$



In [73]:

    
clausula_unit([b])









    



Hemos encontrado una clausula unit  b
[]






    Out[73]:





$$\left [ \right ]$$



In [74]:

    
inconsistente([a,b])









    



Hemos encontrado una clausula unit  a
[b]
Hemos encontrado una clausula unit  b
[]
Hemos llegado al conjunto vacío






    Out[74]:





False



In [75]:

    
inconsistente([~a|b,a,~b])









    



Hemos encontrado una clausula unit  a
[b, ¬b]
Hemos encontrado una clausula unit  b
[False]
Hemos encontrado la cláusula vacía






    Out[75]:





True

Este último ejemplo es precisamente el modus ponens



In [76]:

    
inconsistente(forma_clausular([a>>b,a,~b]))









    



Hemos encontrado una clausula unit  a
[b, ¬b]
Hemos encontrado una clausula unit  b
[False]
Hemos encontrado la cláusula vacía






    Out[76]:





True

Ejemplo Veamos que $(a\to (b\to c))\to(\neg (a\to \neg b)\to c)$ es una tautología. Esto equivale a probar $$\models (a\to (b\to c))\to(\neg (a\to \neg b)\to c).$$ Por el Teorema de la deducción (dos veces), basta probar que $$\{a\to (b\to c), \neg (a\to \neg b)\}\models c,$$ y esto es equivalente a demostrar que el conjunto $$\{a\to (b\to c), \neg (a\to \neg b),\neg c\}$$ es insatisfacible



In [77]:

    
forma_clausular([a>>(b>>c), ~(a>>~b), ~c])









    Out[77]:





$$\left\{a, b, \neg c, c \vee \neg a \vee \neg b\right\}$$



In [78]:

    
inconsistente(_)









    



Hemos encontrado una clausula unit  Not(c)
[¬a ∨ ¬b, b, a]
Hemos encontrado una clausula unit  b
[¬a, a]
Hemos encontrado una clausula unit  Not(a)
[False]
Hemos encontrado la cláusula vacía






    Out[78]:





True

Ejemplo Veamos que $$\{(a\to \neg b\vee d)\wedge(b\wedge \neg d\to a\vee c), (d\to (a \leftrightarrow \neg b)\vee (b\wedge \neg c)\}\models (\neg b\to (d\wedge (c\vee \neg d)))\to c\wedge d$$



In [79]:

    
Gamma={(a>>(~b|d))&((b&~d)>>(a|c)), (d>>(Equivalent(a,~b))|(b|~c)),
       (~b>>(d&(c|~d))),~(c&d)}



In [80]:

    
forma_clausular(Gamma)









    Out[80]:





$$\left\{b \vee d, \neg c \vee \neg d, b \vee c \vee \neg d, d \vee \neg a \vee \neg b, a \vee b \vee \neg c \vee \neg d, a \vee c \vee d \vee \neg b, b \vee \neg a \vee \neg b \vee \neg c \vee \neg d\right\}$$



In [81]:

    
inconsistente(forma_clausular(Gamma))









    



Dividimos usando  Not(c)
set([¬d, b ∨ d, d ∨ ¬a ∨ ¬b])
set([b ∨ d, b ∨ ¬d, a ∨ d ∨ ¬b, d ∨ ¬a ∨ ¬b])
Hemos encontrado una clausula unit  Not(d)
[b, ¬a ∨ ¬b]
Hemos encontrado una clausula unit  b
[¬a]
Hemos encontrado una clausula unit  Not(a)
[]
Hemos llegado al conjunto vacío






    Out[81]:





False

Resolventes



In [82]:

    
Or(Or(a,b),Or(a,c))









    Out[82]:





$$a \vee b \vee c$$



In [83]:

    
def resolventes(a,b):
    literales=[l for l in clausula_a_lista(a) if complemento(l) in clausula_a_lista(b)]
    return [Or(quita(a,l),quita(b,complemento(l))) for l in literales]



In [84]:

    
resolventes(~a|b,a|~b)









    Out[84]:





$$\left [ a \vee \neg a, \quad b \vee \neg b\right ]$$